<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
	<head>
		<title>Binding and Substitution</title>
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
		<meta name="viewport" content="width=device-width initial-scale=1">
		<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
		<meta http-equiv="Content-Language" content="en-gb">

<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
<script>
MathJax = {
	tex: {
		inlineMath: '$', '$'], ['\\(', '\\)'
	},
	svg: {
		fontCache: 'global'
	}
};
</script>
<script type="text/javascript" id="MathJax-script" async
	src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>

<script>
function togglePopup(material_id) {
  var popup = document.getElementById(material_id);
  popup.classList.toggle("show");
}
</script>

<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
		
	</head>
	<body class="commentary-font">
		<nav role="navigation">
		<h1><a href="../index.html"><img src="../docs-assets/Inform.png" height=72> </a></h1>
<ul><li><a href="../index.html">home</a></li>
</ul><h2>Compiler</h2><ul>
<li><a href="../structure.html">structure</a></li>
<li><a href="../inbuildn.html">inbuild</a></li>
<li><a href="../inform7n.html">inform7</a></li>
<li><a href="../intern.html">inter</a></li>
<li><a href="../services.html">services</a></li>
<li><a href="../secrets.html">secrets</a></li>
</ul><h2>Other Tools</h2><ul>
<li><a href="../inblorbn.html">inblorb</a></li>
<li><a href="../inform6.html">inform6</a></li>
<li><a href="../inpolicyn.html">inpolicy</a></li>
</ul><h2>Resources</h2><ul>
<li><a href="../extensions.html">extensions</a></li>
<li><a href="../kits.html">kits</a></li>
</ul><h2>Repository</h2><ul>
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=0> github</a></li>
</ul><h2>Related Projects</h2><ul>
<li><a href="https://github.com/ganelson/inweb"><img src="../docs-assets/github.png" height=0> inweb</a></li>
<li><a href="https://github.com/ganelson/intest"><img src="../docs-assets/github.png" height=0> intest</a></li>
</ul>
		</nav>
		<main role="main">
		<!-- Weave of 'Binding and Substitution' generated by inweb -->
<div class="breadcrumbs">
    <ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#4">Chapter 4: Propositions</a></li><li><b>Binding and Substitution</b></li></ul></div>
<p class="purpose">To substitute constants into propositions in place of variables, and to apply quantifiers to bind any unbound variables.</p>

<ul class="toc"><li><a href="4-bas.html#SP1">&#167;1. Status of variables</a></li><li><a href="4-bas.html#SP9">&#167;9. Getting rid of free variables</a></li><li><a href="4-bas.html#SP14">&#167;14. A footnote on variable 0</a></li><li><a href="4-bas.html#SP17">&#167;17. Unbinding</a></li><li><a href="4-bas.html#SP18">&#167;18. Detect locals</a></li></ul><hr class="tocbar">

<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. Status of variables.</b>In any proposition \(\phi\), we say that a variable \(v\) is "bound" if it
appears as the variable governed by a quantifier: it is "free" if it
does appear somewhere in \(\phi\) &mdash; either directly as a term or indirectly
through a function application &mdash; and is not bound. For instance, in
$$ \forall x : K(x) \land B(x, f_C(y)) $$
the variable \(x\) is bound and the variable \(y\) is free.
</p>

<p class="commentary">In any given proposition, each of the 26 variables always satisfies exactly
one of the following:
</p>

<ul class="items"><li>(a) it is unused if it is never mentioned as, or in, any term, and is not the
variable of any quantifier;
</li><li>(b) it is bound if it appears as the variable of any <span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span>;
</li><li>(c) it is free if it is used but not bound.
</li></ul>
<p class="commentary">The following shows some examples of operations on variables:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">variables in &lt;&lt; &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> valid:</span>
<span class="plain-syntax">'</span><span class="element-syntax">variables in &lt;&lt; even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> valid: x free</span>
<span class="plain-syntax">'</span><span class="element-syntax">set P to &lt;&lt; Forall x IN&lt; kind = number (x) IN&gt;: (x == y) ^ Exists z: (y == z) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> p set to &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : (x == y) ^ Exists z : (y == z) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">variables in P</span><span class="plain-syntax">':</span><span class="string-syntax"> valid: x bound y free z bound</span>
<span class="plain-syntax">'</span><span class="element-syntax">variable unused in &lt;&lt; &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> x</span>
<span class="plain-syntax">'</span><span class="element-syntax">variable unused in P</span><span class="plain-syntax">':</span><span class="string-syntax"> a</span>
<span class="plain-syntax">'</span><span class="element-syntax">renumbering of &lt;&lt; even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">renumbering of &lt;&lt; even (z) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">renumbering of &lt;&lt; Exists z: even (z) ^ (z == y) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; Exists x : even(x) ^ (x == y) &gt;&gt;</span>
</pre>
<p class="commentary">It might seem logical to have a function which takes a proposition \(\phi\)
and a variable \(v\) and returns its status &mdash; unused, free or bound. But this
would be inefficient, since we want to work with all 26 at once, so instead
we take a pointer to an array of <span class="extract"><span class="extract-syntax">int</span></span> which needs to have (at least, but
probably exactly) 26 entries, and on exit each entry is set to one of the
following.
</p>

<p class="commentary">In the course of doing that, it's easy to test whether variables are used
properly &mdash; a bound variable should occur for the first time in its
quantification, and should not reoccur once the subexpression holding the
quantifier has finished. We return <span class="extract"><span class="extract-syntax">TRUE</span></span> if all is well, or <span class="extract"><span class="extract-syntax">FALSE</span></span> if not,
writing the reason why not to <span class="extract"><span class="extract-syntax">err</span></span>.
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">FREE_VST</span><span class="plain-syntax"> </span><span class="constant-syntax">2</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">BOUND_VST</span><span class="plain-syntax"> </span><span class="constant-syntax">3</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::determine_status</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">Binding::determine_status</span></span>:<br/><a href="4-bas.html#SP2">&#167;2</a>, <a href="4-bas.html#SP3">&#167;3</a>, <a href="4-bas.html#SP4">&#167;4</a>, <a href="4-bas.html#SP5">&#167;5</a>, <a href="4-bas.html#SP8">&#167;8</a>, <a href="4-bas.html#SP10">&#167;10</a><br/>Type Check Propositions - <a href="4-tcp.html#SP4_7">&#167;4.7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">text_stream</span><span class="plain-syntax"> *</span><span class="identifier-syntax">err</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">unavailable</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">, </span><span class="identifier-syntax">valid</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) { </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">; </span><span class="identifier-syntax">unavailable</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="constant-syntax">0</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">--;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">unavailable</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] &gt; </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">) </span><span class="identifier-syntax">unavailable</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = -1;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;p-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">26</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"corrupted variable term"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">valid</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">unavailable</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] == -1) {</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">valid</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"%c unavailable"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">]);</span>
<span class="plain-syntax">                }</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] != </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                        </span><span class="identifier-syntax">valid</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                        </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"%c used outside its binding"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">]);</span>
<span class="plain-syntax">                    }</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="constant-syntax">BOUND_VST</span><span class="plain-syntax">; </span><span class="identifier-syntax">unavailable</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] == </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">) </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="constant-syntax">FREE_VST</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                }</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">valid</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>&#167;2. </b>With just a little wrapping, this gives us the test of well-formedness.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::is_well_formed</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">Binding::is_well_formed</span></span>:<br/><a href="4-bas.html#SP13">&#167;13</a><br/>Type Check Propositions - <a href="4-tcp.html#SP4">&#167;4</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_8">&#167;2.8</a>, <a href="5-sc.html#SP9_2">&#167;9.2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">text_stream</span><span class="plain-syntax"> *</span><span class="identifier-syntax">err</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP10" class="function-link"><span class="function-syntax">Propositions::is_syntactically_valid</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">err</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">, </span><span class="identifier-syntax">err</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>&#167;3. </b>Occasionally we really do care only about one of the 26 variables:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::status</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">Binding::status</span></span>:<br/><a href="4-bas.html#SP13_1">&#167;13.1</a><br/>Sentence Conversions - <a href="5-sc.html#SP9_2">&#167;9.2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> == -1) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">];</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>&#167;4. </b>To distinguish sentences from descriptions, the following can be informative:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::number_free</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Binding::number_free</span></span>:<br/><a href="4-bas.html#SP17">&#167;17</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_8">&#167;2.8</a>, <a href="5-sc.html#SP9_2">&#167;9.2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0, </span><span class="identifier-syntax">c</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] == </span><span class="constant-syntax">FREE_VST</span><span class="plain-syntax">) </span><span class="identifier-syntax">c</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"There %s %d free variable%s in $D\n"</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        (</span><span class="identifier-syntax">c</span><span class="plain-syntax">==1)?</span><span class="string-syntax">"is"</span><span class="plain-syntax">:</span><span class="string-syntax">"are"</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax">, (</span><span class="identifier-syntax">c</span><span class="plain-syntax">==1)?</span><span class="string-syntax">""</span><span class="plain-syntax">:</span><span class="string-syntax">"s"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>&#167;5. </b>While this gives us a new variable which can safely be added to an existing
proposition:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::find_unused</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">Binding::find_unused</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP9_7">&#167;9.7</a><br/>Simplifications - <a href="5-smp.html#SP2_1">&#167;2.1</a>, <a href="5-smp.html#SP4">&#167;4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] == </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">25</span><span class="plain-syntax">; </span><span class="comment-syntax"> the best we can do: it avoids crashes, at least...</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>&#167;6. </b>Another "vector operation" on variables: to renumber them throughout a
proposition according to a map array. If <span class="extract"><span class="extract-syntax">renumber_map[j]</span></span> is \(-1\), make
no change; otherwise each instance of variable \(j\) should be changed to
this new number.
</p>

<p class="commentary">In general, it is dangerous to renumber any variable to another which is
already used in the same proposition: that way we could accidentally change
"\(v\) is greater than \(w\)" into "\(w\) is greater than \(w\)", thus changing the
meaning.
</p>

<p class="commentary">Note that because <span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span>s store the variable being quantified
as a term, the following changes quantification variables as well as
predicate terms, which is as it should be.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::vars_map</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">Binding::vars_map</span></span>:<br/><a href="4-bas.html#SP7">&#167;7</a>, <a href="4-bas.html#SP8">&#167;8</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">preserving</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;p-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = &amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
<span class="plain-syntax">            </span><a href="4-bas.html#SP6" class="function-link"><span class="function-syntax">Binding::term_map</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">preserving</span><span class="plain-syntax">) </span><a href="4-bas.html#SP6" class="function-link"><span class="function-syntax">Binding::term_map</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">preserving</span><span class="plain-syntax">, </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::term_map</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><span class="identifier-syntax">pt</span><span class="plain-syntax">=&amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variable</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">nv</span><span class="plain-syntax"> = </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variable</span><span class="plain-syntax">];</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">nv</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">nv</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">26</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"malformed renumbering map"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variable</span><span class="plain-syntax"> = </span><span class="identifier-syntax">nv</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>&#167;7. </b>The following takes any proposition and edits it so that the variables
used are the lowest-numbered ones; moreover, variables are introduced
in numerical order &mdash; that is, the first mentioned will be \(x\), then the
next introduced will be \(y\), and so on.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::renumber</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Binding::renumber</span></span>:<br/><a href="4-bas.html#SP10">&#167;10</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_8">&#167;2.8</a><br/>Simplifications - <a href="5-smp.html#SP14">&#167;14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">preserving</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = -1;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">k</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;p-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] == -1)) </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">k</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-bas.html#SP6" class="function-link"><span class="function-syntax">Binding::vars_map</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">, </span><span class="identifier-syntax">preserving</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>&#167;8. </b>This more complicated routine renumbers bound variables in one proposition
in order to guarantee that none of them coincides with a variable used
in a second proposition. This is needed in order to take the conjunction of
two propositions, because "for all \(x\), \(x\) is a door" and "there exists \(x\)
such that \(x\) is a container" mean different things by \(x\); they can only
be combined in a single proposition if one of the \(x\) variables is changed
to, say, \(y\).
</p>

<p class="commentary">The surprising thing here is the asymmetry. Why do we only renumber to avoid
clashes with bound variables in <span class="extract"><span class="extract-syntax">prop</span></span> &mdash; why not free ones as well? The
answer is that we use a form of conjunction in Inform which assumes that a
free variable in \(\phi\) has the same meaning as it does in \(\psi\); thus in
conjoining "open" with "lockable" we assume that the same thing is meant
to be both open and lockable. If we renumbered to avoid clashes in free
variables, we would produce a proposition meaning that one unknown thing is
open, and another one lockable: that would have two free variables and be
much harder to interpret.
</p>

<p class="commentary">If we pass a <span class="extract"><span class="extract-syntax">query</span></span> parameter which is a valid variable number, the routine
returns its new identity when renumbered.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::renumber_bound</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Binding::renumber_bound</span></span>:<br/>Propositions - <a href="4-prp.html#SP15">&#167;15</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_7">&#167;2.7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">not_to_overlap</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">query</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop_vstates</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">nto_vstates</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">next_unused</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop_vstates</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">not_to_overlap</span><span class="plain-syntax">, </span><span class="identifier-syntax">nto_vstates</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0, </span><span class="identifier-syntax">next_unused</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop_vstates</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] == </span><span class="constant-syntax">BOUND_VST</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">nto_vstates</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] != </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="named-paragraph-container code-font"><a href="4-bas.html#SP8_1" class="named-paragraph-link"><span class="named-paragraph">Advance to the next variable not used in either proposition</span><span class="named-paragraph-number">8.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">next_unused</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = -1;</span>

<span class="plain-syntax">    </span><a href="4-bas.html#SP6" class="function-link"><span class="function-syntax">Binding::vars_map</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">query</span><span class="plain-syntax"> == -1) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> -1;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">query</span><span class="plain-syntax">] == -1) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">query</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">renumber_map</span><span class="plain-syntax">[</span><span class="identifier-syntax">query</span><span class="plain-syntax">];</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP8_1" class="paragraph-anchor"></a><b>&#167;8.1. </b>Again, we fall back on variable 25 if we run out. (This can only happen if
the conjunction of the two propositions had 26 variables.)
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Advance to the next variable not used in either proposition</span><span class="named-paragraph-number">8.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">k</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">k</span><span class="plain-syntax">=</span><span class="identifier-syntax">next_unused</span><span class="plain-syntax">; (</span><span class="identifier-syntax">k</span><span class="plain-syntax">&lt;26) &amp;&amp;</span>
<span class="plain-syntax">        (!((</span><span class="identifier-syntax">prop_vstates</span><span class="plain-syntax">[</span><span class="identifier-syntax">k</span><span class="plain-syntax">] == </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">nto_vstates</span><span class="plain-syntax">[</span><span class="identifier-syntax">k</span><span class="plain-syntax">] == </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">))); </span><span class="identifier-syntax">k</span><span class="plain-syntax">++) ;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">k</span><span class="plain-syntax"> == </span><span class="constant-syntax">26</span><span class="plain-syntax">) </span><span class="identifier-syntax">next_unused</span><span class="plain-syntax"> = </span><span class="constant-syntax">25</span><span class="plain-syntax">; </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">next_unused</span><span class="plain-syntax"> = </span><span class="identifier-syntax">k</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-bas.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>&#167;9. Getting rid of free variables.</b>Propositions with free variables are vague, and Inform tries to minimise its
use of them. Whole verb phrases such as "the tree is in the Courtyard" can in
general become propositions with no free variables, while descriptions such as
"open containers which are in lighted rooms" will become propositions in which
only variable 0, <span class="extract"><span class="extract-syntax">x</span></span>, is free.
</p>

<p class="commentary">Here we see two ways to remove a free variable from a proposition:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">set P to &lt;&lt; Forall x IN&lt; kind = number (x) IN&gt;: (x == y) ^ Exists z: (y == z) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> p set to &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : (x == y) ^ Exists z : (y == z) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">variables in P</span><span class="plain-syntax">':</span><span class="string-syntax"> valid: x bound y free z bound</span>
<span class="plain-syntax">'</span><span class="element-syntax">binding of P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; Exists y : ForAll x IN&lt; kind=number(x) IN&gt; : (x == y) ^ Exists z : (y == z) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">variables in binding of P</span><span class="plain-syntax">':</span><span class="string-syntax"> valid: x bound y bound z bound</span>
<span class="plain-syntax">'</span><span class="element-syntax">substitution of y = 777 in P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : (x == '777') ^ Exists z : ('777' == z) &gt;&gt;</span>
</pre>
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>&#167;10. </b>The first way is "binding". Suppose <span class="extract"><span class="extract-syntax">x</span></span> is free and we do not know its
value. We can at least put <span class="extract"><span class="extract-syntax">Exists x :</span></span> at the front of the proposition, thus
saying only "well, it's something". This does the equivalent of turning "open
containers which are in lighted rooms" into "an open container is in a lighted
room", by applying the existential quantifier to anything free.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::bind_existential</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Binding::bind_existential</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_3">&#167;2.3</a>, <a href="5-sc.html#SP2_6">&#167;2.6</a>, <a href="5-sc.html#SP9_7">&#167;9.7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">preserving</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><a href="4-bas.html#SP7" class="function-link"><span class="function-syntax">Binding::renumber</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">preserving</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=25; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&gt;=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">--)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] == </span><span class="constant-syntax">FREE_VST</span><span class="plain-syntax">)</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><a href="4-ap.html#SP6" class="function-link"><span class="function-syntax">Atoms::QUANTIFIER_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">, </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="constant-syntax">0</span><span class="plain-syntax">));</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>&#167;11. </b>The second way is "substitution", for use when we do know the value of the
free variable we want to remove. We replace every mention of it with some
other term: but as we shall see, this is trickier than it seems.
</p>

<p class="commentary">We begin with two utility routines to substitute into the variable "underneath"
a given term.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::substitute_v_in_term</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Binding::substitute_v_in_term</span></span>:<br/><a href="4-bas.html#SP13">&#167;13</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">t</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">v</span><span class="plain-syntax">) { *</span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = *</span><span class="identifier-syntax">t</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-bas.html#SP11" class="function-link"><span class="function-syntax">Binding::substitute_v_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="identifier-syntax">t</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::substitute_nothing_in_term</span><button class="popup" onclick="togglePopup('usagePopup11')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup11">Usage of <span class="code-font"><span class="function-syntax">Binding::substitute_nothing_in_term</span></span>:<br/>Simplifications - <a href="5-smp.html#SP2_1">&#167;2.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">t</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">DETECT_NOTHING_CALCULUS_CALLBACK</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">DETECT_NOTHING_CALCULUS_CALLBACK</span><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">))) { *</span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = *</span><span class="identifier-syntax">t</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><a href="4-bas.html#SP11" class="function-link"><span class="function-syntax">Binding::substitute_nothing_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">t</span><span class="plain-syntax">);</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::substitute_term_in_term</span><button class="popup" onclick="togglePopup('usagePopup12')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup12">Usage of <span class="code-font"><span class="function-syntax">Binding::substitute_term_in_term</span></span>:<br/>Simplifications - <a href="5-smp.html#SP4">&#167;4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">t</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">) { *</span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = *</span><span class="identifier-syntax">t</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><a href="4-bas.html#SP11" class="function-link"><span class="function-syntax">Binding::substitute_term_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">t</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>&#167;12. </b>Now the main procedure. This is one of those deceptive problems where the
actual algorithm is obvious, but the circumstances when it can validly be
applied are less so.
</p>

<p class="commentary">The difficulty depends on the term \(T\) being substituted in for the variable
\(v\). In general every term is a chain of functions with, right at the end,
either a constant or a variable. If a constant is underneath, there is no
problem at all. But if there is a variable underneath \(T\) &mdash; a VUT, as we
say below &mdash; then it's possible that the substitution introduces circularities
which would make it invalid. If that happens, we run into this:
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="identifier-syntax">DISALLOW</span><span class="plain-syntax">(</span><span class="identifier-syntax">msg</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">verify_only</span><span class="plain-syntax">) { *</span><span class="identifier-syntax">allowed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="identifier-syntax">msg</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>&#167;13. </b>So the routine is intended to be called twice: once to ask if the situation
looks viable, and once to perform the substitution itself.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::substitute_term</span><button class="popup" onclick="togglePopup('usagePopup13')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup13">Usage of <span class="code-font"><span class="function-syntax">Binding::substitute_term</span></span>:<br/><a href="4-bas.html#SP15">&#167;15</a><br/>Simplifications - <a href="5-smp.html#SP14">&#167;14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">t</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">verify_only</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">allowed</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">verify_only</span><span class="plain-syntax">) *</span><span class="identifier-syntax">allowed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">v</span><span class="plain-syntax">&lt;0) || (</span><span class="identifier-syntax">v</span><span class="plain-syntax">&gt;=26)) </span><span class="identifier-syntax">DISALLOW</span><span class="plain-syntax">(</span><span class="string-syntax">"variable substitution out of range"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-bas.html#SP2" class="function-link"><span class="function-syntax">Binding::is_well_formed</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">DISALLOW</span><span class="plain-syntax">(</span><span class="string-syntax">"substituting into malformed prop"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-bas.html#SP13_1" class="named-paragraph-link"><span class="named-paragraph">Make sure the substitution would not fail because of a circularity</span><span class="named-paragraph-number">13.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">verify_only</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        </span><span class="string-syntax">"Substituting %c = $0 in: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">], &amp;</span><span class="identifier-syntax">t</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="function-syntax">&lt;p-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-bas.html#SP11" class="function-link"><span class="function-syntax">Binding::substitute_v_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]), </span><span class="identifier-syntax">v</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">t</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-bas.html#SP2" class="function-link"><span class="function-syntax">Binding::is_well_formed</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"substitution made malformed prop"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP13_1" class="paragraph-anchor"></a><b>&#167;13.1. </b>The problem we might find, then, is that setting \(v=T\) will be circular
because \(T\) itself depends on \(v\). There are two ways this can happen: first,
\(T\) might be directly a function of \(v\) itself, i.e., the VUT might be \(v\);
second, \(T\) might be a function of some variable \(w\) which, by being quantified
after \(v\), is allowed to depend on it, in some way that we can't determine.
</p>

<p class="commentary">The general rule, then, is that \(T\) can contain only constants or variables
which are free within and after the scope of \(v\). (If \(w\) is bound
outside the scope of \(v\) but after it, this means \(w\) didn't exist at the
time that \(v\) did, and the attempted substitution would produce a proposition
which isn't well-formed &mdash; \(w\) would occur before its quantifier.) We can
check this condition pretty easily, it turns out:
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Make sure the substitution would not fail because of a circularity</span><span class="named-paragraph-number">13.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">verify_only</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) &amp;&amp; (</span><a href="4-bas.html#SP3" class="function-link"><span class="function-syntax">Binding::status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">v</span><span class="plain-syntax">) == </span><span class="constant-syntax">BOUND_VST</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">DISALLOW</span><span class="plain-syntax">(</span><span class="string-syntax">"substituting bound variable"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">vut</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;</span><span class="identifier-syntax">t</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">vut</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v_has_been_seen</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> == </span><span class="identifier-syntax">vut</span><span class="plain-syntax">) </span><span class="identifier-syntax">DISALLOW</span><span class="plain-syntax">(</span><span class="string-syntax">"resubstituting same variable"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v_has_been_seen</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="function-syntax">&lt;p-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">])) == </span><span class="identifier-syntax">v</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                        </span><span class="identifier-syntax">v_has_been_seen</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">vut</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax">                (</span><span class="identifier-syntax">v_has_been_seen</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">DISALLOW</span><span class="plain-syntax">(</span><span class="string-syntax">"substituted value may be circular"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-bas.html#SP13">&#167;13</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>&#167;14. A footnote on variable 0.</b>Because of the special status of \(x\) (variable 0) &mdash; the one allowed to be
free in SN-propositions &mdash; we sometimes need to know about it. The range
of a bound variable can be found by looking at its quantifier, but a free
variable can remain ambiguous. The presence of a "kind" atom will explicitly
solve the problem for us; if we don't find one, though, we will simply have
to assume that the set of objects is the domain of \(x\). (We return <span class="extract"><span class="extract-syntax">NULL</span></span>
here, but that's the assumption which the caller will have to make.)
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::kind_of_variable_0</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">))</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>&#167;15. </b>And a quick way to substitute it:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::substitute_var_0_in</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">bogus</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-bas.html#SP13" class="function-link"><span class="function-syntax">Binding::substitute_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">0</span><span class="plain-syntax">, </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">), </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">bogus</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>&#167;16. </b>If we are willing to work a little harder:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::infer_kind_of_variable_0</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-upf.html#SP8" class="function-link"><span class="function-syntax">UnaryPredicateFamilies::infer_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP17" class="paragraph-anchor"></a><b>&#167;17. Unbinding.</b></p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Binding::unbind</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) &amp;&amp; (</span><a href="4-bas.html#SP4" class="function-link"><span class="function-syntax">Binding::number_free</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) == </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)))</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP18" class="paragraph-anchor"></a><b>&#167;18. Detect locals.</b>Properly speaking, this has nothing to do with variables, but it solves a similar
problem.
</p>

<p class="commentary">Here we search a proposition to look for any term involving a local variable.
This is used to verify past tense propositions, which cannot rely on local
values because their contents may have been wiped and reused many times
since the time with which the proposition is concerned.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::detect_locals</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> **</span><span class="identifier-syntax">example</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">, </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="function-syntax">&lt;pl-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax"> =</span>
<span class="plain-syntax">                </span><a href="4-bas.html#SP18" class="function-link"><span class="function-syntax">Binding::detect_local_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]), </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">example</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::detect_local_in_term</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> **</span><span class="identifier-syntax">example</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax"> += </span><a href="4-bas.html#SP18" class="function-link"><span class="function-syntax">Binding::detect_local_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">example</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax"> += </span><a href="4-bas.html#SP18" class="function-link"><span class="function-syntax">Binding::detect_local_in_spec</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">, </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">example</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Binding::detect_local_in_spec</span><span class="plain-syntax">(</span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> **</span><span class="identifier-syntax">example</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">spec</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Lvalues::get_storage_form</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) == </span><span class="identifier-syntax">LOCAL_VARIABLE_NT</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">example</span><span class="plain-syntax">) &amp;&amp; (*</span><span class="identifier-syntax">example</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) *</span><span class="identifier-syntax">example</span><span class="plain-syntax"> = </span><span class="identifier-syntax">spec</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> ++</span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Lvalues::get_storage_form</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NONLOCAL_VARIABLE_NT</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">nonlocal_variable</span><span class="plain-syntax"> *</span><span class="identifier-syntax">nlv</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Node::get_constant_nonlocal_variable</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">NonlocalVariables::is_global</span><span class="plain-syntax">(</span><span class="identifier-syntax">nlv</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">example</span><span class="plain-syntax">) &amp;&amp; (*</span><span class="identifier-syntax">example</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) *</span><span class="identifier-syntax">example</span><span class="plain-syntax"> = </span><span class="identifier-syntax">spec</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> ++</span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Specifications::is_phrasal</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">inv</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">LOOP_THROUGH_INVOCATION_LIST</span><span class="plain-syntax">(</span><span class="identifier-syntax">inv</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">down</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">down</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">tc</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Invocations::get_no_tokens</span><span class="plain-syntax">(</span><span class="identifier-syntax">inv</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;</span><span class="identifier-syntax">tc</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">param</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Invocations::get_token_as_parsed</span><span class="plain-syntax">(</span><span class="identifier-syntax">inv</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax"> +=</span>
<span class="plain-syntax">                    </span><a href="4-bas.html#SP18" class="function-link"><span class="function-syntax">Binding::detect_local_in_spec</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">param</span><span class="plain-syntax">, </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">example</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">spec</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">down</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax"> +=</span>
<span class="plain-syntax">            </span><a href="4-bas.html#SP18" class="function-link"><span class="function-syntax">Binding::detect_local_in_spec</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">, </span><span class="identifier-syntax">example</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">locals_count</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
</pre>
<nav role="progress"><div class="progresscontainer">
    <ul class="progressbar"><li class="progressprev"><a href="4-prp.html">&#10094;</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bpf.html">3</a></li><li class="progresscurrentchapter">4</li><li class="progresssection"><a href="4-trm.html">trm</a></li><li class="progresssection"><a href="4-ap.html">ap</a></li><li class="progresssection"><a href="4-prp.html">prp</a></li><li class="progresscurrent">bas</li><li class="progresssection"><a href="4-tcp.html">tcp</a></li><li class="progresschapter"><a href="5-sc.html">5</a></li><li class="progressnext"><a href="4-tcp.html">&#10095;</a></li></ul></div>
</nav><!-- End of weave -->

		</main>
	</body>
</html>

